I like the generics-sop way of modeling generic types as a promoted list of list of types: `[[Type]]`

. "Sums of products" represents `Bool`

with two constructors (sums) generically as a list of length two. The inner lists represent the arguments of the constructors (products).

Since `False`

and `True`

take no arguments the inner lists of `Code Bool`

= `'[ '[], '[] ]`

are empty.

```
> import Generics.SOP
>
> :kind! Code Bool
Code Bool :: [[*]]
= '[ '[], '[]]
> :kind! Code (Maybe Int)
Code (Maybe Int) :: [[*]]
= '[ '[], '[Int]]
> :kind! Code (Either Int Bool)
Code (Either Int Bool) :: [[*]]
= '[ '[Int], '[Bool]]
> :kind! Code ((), (), (), (), ())
Code ((), (), (), (), ()) :: [[*]]
= '[ '[(), (), (), (), ()]]
```

It is easy to define a `GenericallySOP`

modifier for generic `Semigroup`

and `Monoid`

instances. I adapted code from here but it's not important to understand the details.

```
type GenercallySOP :: Type -> Type
newtype GenercallySOP a = GenercallySOP a
instance
( SOP.Generic a
, IsProductType a as
, SOP.All Semigroup as
) => Semigroup (GenercallySOP a) where
(<>) :: GenercallySOP a -> GenercallySOP a -> GenercallySOP a
(<>) = coerce m where
m :: a -> a -> a
m (from -> SOP (Z as)) (from -> SOP (Z bs)) =
to $ SOP $ Z $ hcliftA2 @_ @Semigroup Proxy (liftA2 (<>)) as bs
instance
( SOP.Generic a
, IsProductType a as
, SOP.All Semigroup as
, SOP.All Monoid as
)
=>
Monoid (GenercallySOP a) where
mempty :: GenercallySOP a
mempty = GenercallySOP $ to $ SOP $ Z $ hcpure @_ @_ @_ @Monoid Proxy (I mempty)
```

This allows us to derive monoid instances assuming that each field of the datatype is a monoid.

```
type Strs :: Type
data Strs = Strs String String
deriving
( Semigroup -- Strs a b <> Strs a' b' = Strs (a++a') (b++b')
, Monoid -- mempty = Strs "" ""
)
via GenericallySOP Strs
```

ah assuming we have derived its `SOP.Generic`

instance which relies on the `GHC.Generic`

instance

```
deriving
stock GHC.Generic
deriving
anyclass SOP.Generic
```

What if some of the fields aren't monoids? What if they are monoids in more ways than one?

Core idea: given two codes `code`

, `code'`

we can safely `(unsafe)Coerce `

their generic representations `SOP I code`

, `SOP I code'`

if the element are coercible (pointwise) (`AllZip2 Coercible code code'`

). Coercible means being represented the same at runtime.This has numerous applications. It's not uncommon to see a datatype that is essentially a product of monoids with non-default behaviour.`Int`

is an example of a type that has no semigroup instance, yet addition and multiplication form a semigroup.`[Bool]`

is a monoid but in more ways than one. As you see we use something more exotic than the normal ++ and [] behaviour of lists.

This also can be derived.

```
--
-- Code (Foo a) = '[ '[ Int, Int, [Bool], a->a ] ]
--
type Foo :: Type -> Type
data Foo a = Foo
{ one :: Int
, two :: Int
, three :: [Bool]
, four :: a->a
}
instance Semigroup (Foo a) where
(<>) :: Foo a -> Foo a -> Foo a
Foo a b cs d <> Foo a' b' cs' d' =
Foo (a + a') (b * b') (zipWith (&&) cs cs') (d . d')
instance Monoid (Foo a) where
mempty :: Foo a
mempty = Foo 0 1 (repeat True) id
```

`newtype`

For a long time we have had generalized newtype deriving which allows deriving via the underlying representation of a datatype. This uses the fact that pairs are monoids if each component is:

```
instance (Semigroup a, Semigroup b) => Semigroup (a, b)
instance (Monoid a, Monoid b) => Monoid (a, b)
```

`Sum Int`

indicates + and 0`Product Int`

indicates * and 1`Ap ZipList All`

indicate zipWith (&&) and repeat True`All`

indicates && and True`Endo a`

indicates . and id

These modifiers give their underlying types different behaviour but they add unsightly noise to the actual constructor:

```
type Foo :: Type -> Type
newtype Foo a = Foo
(Sum Int, Product Int, Ap ZipList All, Endo a)
deriving
newtype (Semigroup, Monoid)
```

`via`

Such low-level details shouldn't matter when using `Foo`

. Deriving via solves that by factoring it out into a via type but leaves a different problem.

```
type Foo :: Type -> Type
newtype Foo a = Foo (Int, Int, [Bool], a->a)
deriving
(Semigroup, Monoid)
via
(Sum Int, Product Int, Ap ZipList All, Endo a)
```

`via`

We want `Foo`

to be curried and to use record syntax. We could reach for pattern synonyms over a `newtype`

but in this case it does not encourage a natural style of writing. We don't want deriving to change our datatype.

```
type Foo :: Type -> Type
data Foo a = Foo
{ one :: Int
, two :: Int
, three :: [Bool]
, four :: a->a
}
deriving
(Semigroup, Monoid)
via
GenericallySOP
(Foo a
`PretendingVia`
'[ '[ Sum Int, Product Int, Ap ZipList All, Endo a ] ])
```

and mandatory deriving generics:

```
deriving stock GHC.Generic
deriving anyclass SOP.Generic
```

This is the heart of this article. `PretendingVia`

hijacks a `SOP.Generic`

instance and injects a custom "*via* code".

```
type PretendingVia :: Type -> [[Type]] -> Type
newtype a `PretendingVia` viacode = PretendingVia
{ pretendVia :: a
}
```

This is based on a single assumption that it is indeed safe to coerce between `Rep a = SOP I (Code a)`

and `SOP I viacode`

:

```
instance
( SOP.All SListI viacode
, Generic a
, AllZip2 Coercible viacode (Code a)
, AllZip2 Coercible (Code a) viacode
)
=>
Generic (PretendingVia a viacode) where
type Code (PretendingVia a viacode) = viacode
to :: SOP I viacode -> PretendingVia a viacode
to = axiom @viacode @(Code a) >>> to >>> PretendingVia
from :: PretendingVia a viacode -> SOP I viacode
from = pretendVia >>> from >>> axiom @(Code a) @viacode
```

expressed as this axiom

```
axiom :: forall code0 code1.
AllZip2 Coercible code0 code1
=> SOP I code0
-> SOP I code1
axiom = unsafeCoerce
```

Attempting to `stock`

derive `Ord Exp`

or `Show Exp`

is not possible because `Exp->Exp`

has none of those instances.

```
--
-- Code Exp = '[ '[Exp, Exp], '[Exp->Exp] ]
--
type Exp :: Type
data Exp = App Exp Exp | Lam (Exp -> Exp)
```

Since `Exp->Exp`

is coercible to `Hidden (Exp->Exp)`

we can view `'[ '[Exp, Exp], '[Hidden (Exp->Exp)] ]`

as the `Exp`

code which ignores the function argument.

```
type Hidden :: Type -> Type
newtype Hidden a = Hidden a
instance Show (Hidden a) where
show :: Hidden a -> String
show _ = "(*)"
instance Eq (Hidden a) where
(==) :: Hidden a -> Hidden a -> Bool
_ == _ = True
instance Ord (Hidden a) where
compare :: Hidden a -> Hidden a -> Ordering
compare _ _ = EQ
```

As before we require an instance of `GenericallySOP`

this time taken directly from `Generics.SOP.Eq`

:

```
instance (Generic a , All2 Eq (Code a)) => Eq (GenercallySOP a) where
(==) :: GenercallySOP a -> GenercallySOP a -> Bool
(==) = coerce (geq @a)
```

This

```
type Exp :: Type
data Exp = App Exp Exp | Lam (Exp -> Exp)
deriving
Eq
via
GenercallySOP
(Exp
`PretendingVia`
'[ '[ Exp, Exp ]
, '[ Hidden (Exp->Exp) ]
])
```

with

```
deriving stock GHC.Generic
deriving anyclass SOP.Generic
```

means you can compare `Lam id == Lam (\f -> App f f)`

for equality. And it gives back `True`

. Well it's possible anyway, and relatively little fuss.

Links

Published with Brick